(*
 * Copyright 2014, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

theory Sep_Rule_Ext
  imports Sep_Provers
          Sep_Attribs
          Sep_ImpI
          Sep_MP
begin



ML {*

   fun backwardise ctxt thm = SOME (backward ctxt thm)
                              handle THM _  => NONE

   fun sep_curry ctxt thm = SOME (sep_curry_inner ctxt thm)
                    handle THM _ => NONE


   fun make_sep_drule direct thms ctxt i =
     let val default = sep_drule_comb_tac direct
         fun make_sep_rule_inner i thm  =
             let val goal = i + Thm.nprems_of thm - 1 in
                     case sep_curry ctxt thm of (SOME thm') =>
                                             (sep_drule_tac (fn i => sep_drule_tactic ctxt [thm'] i THEN
                                              ((sep_mp_solver ctxt) THEN' (TRY o sep_flatten ctxt)) goal ) ctxt) i|
                                         NONE => default [thm] ctxt i
                     end;
      in if direct then default thms ctxt i else FIRST (map (make_sep_rule_inner i) thms )
    end;


   fun make_sep_rule direct thms ctxt =
     let val default = sep_rule_comb_tac direct
         fun make_sep_rule_inner thm = case backwardise ctxt thm of
                                  (SOME thm') => sep_rule_comb_tac true [thm'] ctxt THEN'
                                                (REPEAT_ALL_NEW (sep_match_trivial_tac ctxt)) THEN'
                                                 (TRY o (sep_flatten ctxt))  |
                                         NONE => default [thm] ctxt
      in if direct then default thms ctxt else  FIRST' (map make_sep_rule_inner thms)
    end;

   fun sep_rule_method direct thms ctxt = SIMPLE_METHOD' (make_sep_rule direct thms ctxt)

   fun sep_drule_method direct thms ctxt = SIMPLE_METHOD' (make_sep_drule direct thms ctxt)
*}

method_setup sep_rule = {*
  (Scan.lift (Args.mode "direct")) -- Attrib.thms  >> uncurry sep_rule_method
*}

method_setup sep_drule = {*
  (Scan.lift (Args.mode "direct")) -- Attrib.thms  >> uncurry sep_drule_method
*}

end
